%==============================================================================
% Enunciado
%==============================================================================

% Formalizar en OTTER la siguiente argumentación y comprobar su validez:
% "Para todo hombre hay una mujer que no conduce peor que él, por tanto el
% mejor conductor del mundo es una mujer."

%==============================================================================
% Formalización
%==============================================================================

set(auto2).

formula_list(sos).

% Para todo hombre hay una mujer que no conduce peor que él
  all x (hombre(x) -> (exists y (mujer(y) & (- conducePeor(y,x))))).

  all x (hombre(x) | mujer(x)).
  all x (hombre(x) -> -mujer(x)).

% La relación '- conducePeor' es transitiva.
  all x y z ((-conducePeor(x,y)) & (-conducePeor(y,z)) -> (-conducePeor(x,z))).

% El mejor conductor del mundo.
  exists y (all x (- conducePeor(y,x))).

% Conclusión: el mejor conductor del mundo es una mujer.
  - (exists y (mujer(y) & (all x (- conducePeor(y,x))))).

end_of_list.

%==============================================================================
